Build CBMC in Visual Studio 2019, in Github Actions. #5459
Conversation
NlightNFotis
commented
Aug 13, 2020
NlightNFotis
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
NlightNFotis
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
| @@ -21,3 +21,22 @@ jobs: | |||
| run: cd build; ninja | |||
| - name: Run CTest | |||
| run: cd build; ctest -V -L CORE . | |||
| check-vs-2019-build-and-test: | |||
There was a problem hiding this comment.
The name of the action is build-and-test because I'm already working on building and running tests on Github Actions under vs2019, but the running tests part is not there yet - however, since the building CBMC is already done, we figured we could publish this part of the work, and get the rest of it merged as it's finished.
There was a problem hiding this comment.
I don’t think this needs to be called ‘build-and-test’, the other jobs in here are called ‘check’-somethingsomething and I think building and testing should be implied.
If you’re doing something other than building and testing that should be called out.
There was a problem hiding this comment.
⛏️ Given that testing isn't part of this PR, we should probably name this check-vs-2019-build-only, so that there is no confusion in the interim between the two PRs. It can just be renamed again, when the second PR comes.
| shell: cmd | ||
| steps: | ||
| - name: Checkout the repository | ||
| uses: actions/checkout@v2 |
There was a problem hiding this comment.
| uses: actions/checkout@v2 | |
| uses: actions/checkout@v2 | |
| with: | |
| submodules: recursive |
| uses: actions/checkout@v2 | ||
|
|
||
| - name: Update the submodules | ||
| run: git submodule update --init |
There was a problem hiding this comment.
Apply above suggestion then this step isn’t needed anymore
| run: git submodule update --init | ||
|
|
||
| - name: Install bison and flex | ||
| run: ${{env.SCRIPT_DIR}}\install-bison.bat |
There was a problem hiding this comment.
It’s in env, so this really should be %SCRIPT_DIR%
| run: ${{env.SCRIPT_DIR}}\install-bison.bat | ||
|
|
||
| - name: Build cbmc | ||
| run: ${{env.SCRIPT_DIR}}\build-cbmc.bat |
There was a problem hiding this comment.
ditto
| @@ -21,3 +21,22 @@ jobs: | |||
| run: cd build; ninja | |||
| - name: Run CTest | |||
| run: cd build; ctest -V -L CORE . | |||
| check-vs-2019-build-and-test: | |||
There was a problem hiding this comment.
⛏️ Given that testing isn't part of this PR, we should probably name this check-vs-2019-build-only, so that there is no confusion in the interim between the two PRs. It can just be renamed again, when the second PR comes.
Codecov Report
@@ Coverage Diff @@
## develop #5459 +/- ##
========================================
Coverage 68.22% 68.22%
========================================
Files 1178 1178
Lines 97580 97580
========================================
Hits 66573 66573
Misses 31007 31007
Flags with carried forward coverage won't be shown. Click here to find out more. Continue to review full report at Codecov.
|
| submodules: recursive | ||
|
|
||
| - name: Install bison and flex | ||
| run: %SCRIPT_DIR%\install-bison.bat |
There was a problem hiding this comment.
🚫 This doesn’t run right now due to a yaml parsing error (apparently % is not allowed in plain context). Write this as either
| run: %SCRIPT_DIR%\install-bison.bat | |
| run: "%SCRIPT_DIR%\\install-bison.bat" |
or
| run: %SCRIPT_DIR%\install-bison.bat | |
| run: | | |
| %SCRIPT_DIR%\install-bison.bat |
NlightNFotis
force-pushed
the
vs-github-action-build
branch
from
aeb0ccd to
a6ca1ab
Compare
